00100	EXPLICIT SETS
00200	
00300	
00400		An  additional  type  of constant recognized by PCHECK is the
00500	explicit set.  An explicit set is given as a list of its members  and
00600	is written SET(a,b,...,c).  An example is
00700	
00800		SET(A,X,SET(A,C),'(A B)).
00900	
01000		The following commands apply to sets:
01100	
01200	1. ISSET(u)
01300		If u has the above form, a line is generating asserting
01400	
01500		ISSET(u).
01600	
01700	The elements of the list are required  to  meet  the  conditions  for
01800	terms.   It  is  not  immediately clear to me whether they have to be
01900	constants or whether terms containing variables are allowed.
02000	
02100	2. MEMBER(x,u)
02200	
02300		If u has the form  of  a  set  and  x  has  the  form  of  an
02400	individual and if x occurs in u, then a line is generated asserting
02500		xεu.
02600	
02700	3. PICK(u)
02800	
02900		If u is SET(a,b,...c),then PICK(u) generates a line asserting
03000	
03100		aεu.
03200	
03300	4. EQUAL(u,v)
03400	
03500		If the lists  of  elements  of  u  and  v  contain  the  same
03600	elements, then the new line is
03700	
03800		u=v.
03900	
04000	Note  that  we  cannot  assert  u≠v  except  in special cases because
04100	expressions that are apparently different may be later proved equal.
04200	
04300	5. UNION(u,v)
04400	
04500		This command forms the union w of the two sets and  generates
04600	a line asserting
04700	
04800		u∪v=w.
04900	
05000		Note  that  intersection,  set  difference,  and  cardinality
05100	commands are not possible unless it is possible to test the  equality
05200	of  elements  of  the  sets.   This  is  possible  for sets of quoted
05300	S-expressions which are guaranteed to be distinct if they  appear  to
05400	be distinct.